Automatic generation produced by ISE Eiffel
indexing
description: "Objects used to hold http session state."
author: "Peizhu Li, <lip@student.ethz.ch>"
date: "20.12.2008"
revision: "$0.6$"
class interface
SESSION
create
make
feature --attributes
session_id: STRING_8
-- save session_id by its own
creation_time: DATE_TIME
-- session creation timestamp
expiration_time: DATE_TIME
-- when session will get expired
object_list: HASH_TABLE [ANY, STRING_8]
-- user injected objects that need to be saved
feature --creation
make
-- initialize a default session object
feature -- access
set_session_id (sid: STRING_8)
-- set session id
require
session_id_valid: sid /= Void and then not sid.is_empty
set_expiration_time (expiration: DATE_TIME)
-- set expiration date
set_expiration_after_seconds (seconds: INTEGER_32)
-- set expiration date to be seconds after now
expired: BOOLEAN
-- whether session is expired
set_attribute (name: STRING_8; obj: ANY)
-- add/update an attribute in session state
require
valid_name_is_given: name /= Void and not name.is_empty
valid_object_is_given: obj /= Void
delete_attribute (name: STRING_8)
-- delete an attribute from state
require
valid_name_is_given: name /= Void and not name.is_empty
attribute_exists: object_list.has (name)
ensure
one_attribute_deleted: object_list.count = old object_list.count - 1
get_attribute (name: STRING_8): ANY
-- retrieve an attribute object from current session state, return void if not exist
require
valid_name_is_given: name /= Void and not name.is_empty
attribute_exists: object_list.has (name)
has_attribute (name: STRING_8): BOOLEAN
-- check whether a specified session object exists
require
valid_name_is_given: name /= Void and not name.is_empty
invariant
invariant_clause: True
end -- class SESSION
-- Generated by ISE Eiffel --
For more details: www.eiffel.com